
In this report we have presented how to model the dynamics of \rsd{s} with Petri nets with timestamps. We will now establish a connection between the model and the toxicity analysis.

As mentioned in the introduction we are mainly interested in addressing two families of problems:  the presence (resp. absence) of a given set of species or the activation (resp. inhibition) of pathways. Observe that these two problems are strictly related and, as a matter of fact, they can be reduced to a single reachability problem. More precisely, both problems can be rephrased in checking whether a certain configuration is reachable.
Indeed, the Petri net model presented above can be used to simulate the behavior of \rsd{s}, moreover we conjecture that the reachability problem is decidable for Petri nets with timestamps.

\paragraph{Example.}
We consider the same example as before and we suppose that $D$ is a dangerous species for the system. So we ask whether there exists a configuration in the simulation of the Petri net where $D$ is produced. At a first glance, it could seem that this is not possible as the lifetime of $B$ is shorter than the duration of the reaction $r_1$. Nevertheless, there exists a run in the system \RS (i.e., a sequence of markings) where $D$ can effectively appear in the system.
Indeed, given the initial marking $m_0$ we have the following:
$$
\begin{array}{l|c|c|c|c|c|c}
 t           & \Pclock & A 		   & B  		    & C 		      & D 		       & E \\
-            &  0         & \tuple{0,0,0}& \tuple{1,0,0} & \tuple{1,0,0} & \tuple{0,0,0} & \tuple{1,0,0} \\
t_c         &  1         & \tuple{0,0,0}& \tuple{1,0,0} & \tuple{1,0,0} & \tuple{0,0,0} & \tuple{1,0,0} \\
t_c         &  2         & \tuple{0,0,0}& \tuple{1,0,0} & \tuple{1,0,0} & \tuple{0,0,0} & \tuple{1,0,0} \\
t_c         &  3         & \tuple{0,0,0}& \tuple{0,0,3} & \tuple{1,0,0} & \tuple{0,0,0} & \tuple{1,0,0} \\
t_c         &  4         & \tuple{0,0,0}& \tuple{0,0,3} & \tuple{1,0,0} & \tuple{0,0,0} & \tuple{1,0,0} \\
t_{r_2}  &  4         & \tuple{1,4,4}& \tuple{0,0,3} & \tuple{1,0,0} & \tuple{0,0,0} & \tuple{1,0,0} \\
t_c         &  5         & \tuple{1,4,4}& \tuple{0,0,3} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_c         &  6         & \tuple{1,4,4}& \tuple{0,0,3} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_{r_3}  &  6         & \tuple{1,4,4}& \tuple{1,6,6} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_c         &  7         & \tuple{1,4,4}& \tuple{1,6,6} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_c         &  8         & \tuple{1,4,4}& \tuple{1,6,6} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_{r_3}  &  8         & \tuple{1,4,4}& \tuple{1,8,6} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_c         &  9         & \tuple{1,4,4}& \tuple{1,8,6} & \tuple{0,0,5} & \tuple{0,0,0} & \tuple{0,0,5} \\
t_{r_1}  &  9         & \tuple{1,4,4}& \tuple{1,9,6} & \tuple{0,0,5} & \tuple{1,9,9} & \tuple{0,0,5} 
\end{array}
$$
where  one can see that in the last step reaction $r_1$ has been performed, thus entailing the production of $D$.

\subsection{Future work} 
As for future work, we aim at firstly addressing the question about reachability. We believe that by appealing to the theory of well structured transition systems \cite{FinkelS01,AbdullaCJT00} we could prove that there exists a well quasi order among markings that is strongly compatible wrt the firing of transitions. This is a sufficient condition to  guarantee that the reachability problem is decidable.
As a second step, we would like to establish an upper bound to the minimal number of steps for reaching each possible configuration. This upper bound will permit us to have a finite representation of the Petri net and thus to be able to use well know tools for efficiently testing the reachability properties mentioned above.

Finally, the model we have presented here, can be extended in several directions. For instance, one can imagine different interpretation for reactions. Here, we have deliberately choose to work with interleaving, but another solution could be to consider maximal concurrency and thus make all enabled reactions to fire in one step.
Another development could be to deal with continuous time instead of discrete time. This solution would be certainly closer to reality but poses a number of problems as for instance it has a negative impact on the complexity of the system: indeed, reachability immediately  becomes undecidable.


